/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.cli;

import gnu.getopt.Getopt;
import gnu.getopt.LongOpt;

import java.io.BufferedInputStream;
import java.io.FileInputStream;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;

import alloy.api.AlloyRunner;
import alloy.api.LiftedUnsatCore;
import alloy.api.SolutionData;
import alloy.api.TranslationException;
import alloy.ast.Command;
import alloy.ast.Commands;
import alloy.ast.DummyNode;
import alloy.ast.FindCommand;
import alloy.ast.IntNode;
import alloy.ast.Location;
import alloy.ast.Node;
import alloy.log.AlloyLog;
import alloy.util.CleanupManager;
import alloy.util.Dbg;
import alloy.util.ParamFormatException;
import alloy.util.Parameter;
import alloy.util.Params;

/**
 * A command-line interface for Alloy that utilizes the Alloy API.
 * 
 * @see alloy.api.AlloyRunner
 * @see gnu.getopt
 */

public class AlloyCLI {

	/**
	 * Info message listener that prints progress/status messages while the tool
	 * is working.
	 */
	private static Dbg.DbgMsgListener _infoListener = new Dbg.DbgMsgStreamPrinter(System.out);

	/** help message */
	private static final String _helpMsg = "Alloy Analyzer command line options:\n"
			+ "  -b solver_name : set boolean solver (MCHAFF, ZCHAFF, or BERKMIN), default MCHAFF\n"
			+ "  -# nsols : return up to this many solutions (default 1)\n" 
			+ "  -N : count solutions\n"
			+ "  -C config_file_name : use alternate configuration file\n"
			+ "  -R command_name : run specific command\n" 
			+ "  -r : disabling detection of shared subformulas\n"
			+ "  -m : disable symmetry breaking\n" 
			+ "  -d : developer options\n"
			+ "  -s : skolemize inside universal quantifiers\n"
			+ "  -e : enable extra clauses for multiple solutions\n" 
			+ "  -c : use compact variable allocation\n"
			+ "  -n : only perform semantic checking, no running of commands\n" 
			+ "  -S : specify random seed\n"
			+ "  -v : verbose output\n" 
			+ "  -E : Emacs-style error-reporting\n" 
			+ "  -h : print help message\n"
			+ "  -o : save Solution to a file\n" 
			+ "  -V : visualize solutions\n" 
			+ "  -f : load Customization file\n"
			+ "  -U : determine unsat core\n" 
			+ "  -a astFileName.xml : write out the AST in XML format\n"
			+ "Return Codes:\n"
			+ "   0 - ok\n"
			+ "   1 - some problem inside Alloy (Dbg.fatal) \n"
			+ "  11 - found some solutions but expected none \n"
			+ "  12 - found no solutions but expected some \n"
			+ "  13 - translation problem \n"
			+ "  14 - compilation problem \n"
			;

	private static final int RC_OK = 0;
	private static final int RC_FOUND_SOME_EXPECTED_NONE = 11;
	private static final int RC_FOUND_NONE_EXPECTED_SOME = 12;
	private static final int RC_TRANSLATION_PROBLEM = 13;
	private static final int RC_COMPILATION_PROBLEM = 14;
	

	/** if <code>true</code>, print verbose output */
	private static boolean _verbose = false;

	/**
	 * if <code>true</code>, checks commands in spec. if <code>false</code>,
	 * checks no commands.
	 */
	private static boolean _checkCommands = true;

	/** Max # of solutions to return. */
	private static long _maxSols = 1;

	/** Whether we should be counting solutions instead of finding one solution */
	private static boolean _countSolutions = false;

	/**
	 * if <code>true</code>, check specific commands named at command-line;
	 * if <code>false</code>, check all commands. only meaningful if
	 * {@link _checkCommands} is <code>true</code>
	 */
	private static boolean _specificCommands = false;

	/**
	 * List of commands to run. Only used if {#link _specificCommands} is
	 * <code>true</code.
	 */
	private static final List _commandNames = new ArrayList(); // List[String]

	/** if <code>true</code>, use Emacs-style error-reporting */
	private static boolean _emacsStyle = false;

	private static boolean _saveSolutionData = false;

	private static boolean _visualize = false;

	private static String _custFile;

	/* File to which to write out the translatable AST in XML format */
	private static String _astFileName;

	private static boolean _loadCust = false;

	/** If true, determine the (lifted) unsat core */
	private static boolean _liftedUnsatCore = false;

	/**
	 * <p>
	 * Run the Alloy Analyzer from the command line.
	 * 
	 * <p>
	 * Command-line format:<br>
	 * 
	 * <pre>
	 * java alloy.cli.AlloyCLI [-b solver_name] [-r] [-m] [-n] [-v] [-h] [module_names]
	 * </pre>
	 */
	public static void main(String[] args_) {
		try {
			final List longOpts = new ArrayList();
			final List helpStrings = new ArrayList();
			final List params = new ArrayList();
			_getConfigInfo(longOpts, helpStrings, params);
			final Getopt g = new Getopt("Alloy Analyzer", args_, "b:#:C:R:rmdsecnvES:hoVf:NUa:", (LongOpt[]) longOpts
					.toArray(new LongOpt[] {}));
			_parseCommandLineArgs(g, longOpts, helpStrings, params);

			if (!_emacsStyle) {
				Dbg.defaultInit();
			} else {
				Dbg.addDbgMsgListener(Dbg.USER, new alloy.cli.AlloyCLI.EmacsMsgListener(System.out));
				Dbg.addDbgMsgListener(Dbg.WARN, Dbg.FATAL, Dbg.UNIMPL, new Dbg.DbgMsgStreamPrinter(System.out,
						Dbg.STACK_FULL));
			}

			if (_verbose)
				_printOptions();

			AlloyLog.logStartSession(AlloyLog.UI);
			for (int i = g.getOptind(); i < args_.length; i++) {
				final int rc = _runAnalyzer(args_[i]);
				if (rc != RC_OK) { // die if it didn't work out ok
					AlloyLog.logEndSession(AlloyLog.UI);
					CleanupManager.exit(rc);					
				}
			}
			AlloyLog.logEndSession(AlloyLog.UI);
		} catch (NumberFormatException nfe_) {
			Dbg.fatal("Invalid number used in option: " + nfe_);
		} catch (Exception t) {
			t.printStackTrace();
			Dbg.fatal("Internal error", t);
		}

		if (!_visualize) {
			CleanupManager.exit(RC_OK);
		}
	} // main

	private static void _getConfigInfo(List longOpts, List helpStrings, List params) {
		StringBuffer sb = new StringBuffer();
		for (Iterator grpNameIter = Params.glob.getGroupNames().iterator(); grpNameIter.hasNext();) {
			String grpName = (String) grpNameIter.next();
			List grpParams = Params.glob.getGroupParams(grpName);
			for (Iterator paramIter = grpParams.iterator(); paramIter.hasNext();) {
				Parameter param = (Parameter) paramIter.next();
				params.add(param);
				String paramOpt = grpName + "." + param.getName();
				longOpts.add(new LongOpt(paramOpt, param.getType() == Parameter.BOOLEAN ? LongOpt.OPTIONAL_ARGUMENT
						: LongOpt.REQUIRED_ARGUMENT, sb, 0));
				StringBuffer helpStr = new StringBuffer("--" + paramOpt);
				switch (param.getType()) {
				case Parameter.BOOLEAN:
					helpStr.append(" " + (param.getValue().equals("0") ? "enable " : "disable ") + param.getMessage());
					break;
				case Parameter.ENUM:
					helpStr.append(" [");
					for (Iterator enumValIter = param.getEnum().values.iterator(); enumValIter.hasNext();) {
						helpStr.append(enumValIter.next());
						if (enumValIter.hasNext())
							helpStr.append("/");
					}
					helpStr.append("] " + param.getMessage());
				default:
					helpStr.append(" " + param.typeString() + " " + param.getMessage());
				}
				helpStrings.add(helpStr.toString());
			} // loop over params in group
		} // loop over parameter groups
	}

	private static void _parseCommandLineArgs(Getopt g, List longOpts, List helpStrings, List params) {
		int curOpt;
		while ((curOpt = g.getopt()) != -1) {
			switch (curOpt) {
			case 0: {
				Parameter param = (Parameter) params.get(g.getLongind());
				if (param.getType() == Parameter.BOOLEAN)
					param.setValue(g.getOptarg().equals("1") ? "1" : "0");
				else
					param.setValue(g.getOptarg());
				break;
			}
			case 'b':
				Params.glob.setParam("MAIN", "solver", g.getOptarg());
				break;
			case 'r':
				Params.glob.setParam("MAIN", "sharbool", false);
				break;
			case 'm':
				Params.glob.setParam("MAIN", "usesymm", false);
				break;
			case 'd':
				Params.glob.setParam("DEVEL", "ringsymm", true);
				break;
			case 's':
				Params.glob.setParam("MAIN", "skoluniv", true);
				break;
			case 'S':
				Params.glob.setParam("MAIN", "randseed", Long.parseLong(g.getOptarg()));
				break;
			case 'e':
				Params.glob.setParam("MAIN", "multsol", true);
				break;
			case 'c':
				Params.glob.setParam("DEVEL", "compalloc", true);
				break;
			case 'n':
				_checkCommands = false;
				break;
			case 'N':
				_countSolutions = true;
				break;
			case '#':
				_maxSols = Long.parseLong(g.getOptarg());
				break;
			case 'C':
				String fileName = g.getOptarg();
				try {
					InputStream paramInput = new BufferedInputStream(new FileInputStream(fileName));
					Params.glob = Params.load(paramInput);
				} catch (IOException e) {
					Dbg.warn("Could not load configuration file " + fileName, e);
				} catch (ParamFormatException e) {
					Dbg.warn("Could not load configuration file " + fileName, e);
				}
				break;
			case 'R':
				_specificCommands = true;
				_commandNames.add(g.getOptarg());
				break;
			case 'v':
				_verbose = true;
				Dbg.addDbgMsgListener(Dbg.INFO, _infoListener);
				break;
			case 'E':
				_emacsStyle = true;
				break;
			case '?':
			case 'o':
				_saveSolutionData = true;
				break;
			case 'V':
				_visualize = true;
				break;
			case 'f':
				_custFile = g.getOptarg();
				_loadCust = true;
				break;
			case 'U':
				_liftedUnsatCore = true;
				break;
			case 'a':
				_astFileName = g.getOptarg();
				break;

			case 'h':
				System.out.println(_helpMsg);
				System.out.println(" Long options: ");
				for (Iterator helpStrIter = helpStrings.iterator(); helpStrIter.hasNext();) {
					System.out.println("          " + helpStrIter.next());
				}
				System.exit(0);
				break;
			default: {
				System.out.println("unknown option: -" + curOpt);
				System.exit(1);
			}
			}

		}
	}

	/** print option settings */
	private static void _printOptions() {
		System.out.println("option values");
		System.out.println("-------------");
		Params.glob.save(System.out);
		System.out.println();
	}

	/** run analyzer on a module */
	private static int _runAnalyzer(String fileName_) {
		final int rc;
		if (!_emacsStyle)
			System.out.println("Compiling " + fileName_ + "...");
		if (AlloyRunner.prepareSpec(fileName_)) {
			System.out.println("Compilation successful!");
			if (_checkCommands) {
				Commands commands = AlloyRunner.getCommands();
				if (_specificCommands) {
					rc = _runSpecificCommands(fileName_, commands);
				} else {
					rc = _runAllCommands(fileName_, commands);
				}
			} else {
				rc = RC_OK;
			}
		} else { // module did not compile
			if (!_emacsStyle)
				System.out.println("Errors compiling module.\n");
			rc = RC_COMPILATION_PROBLEM;
		}
		return rc;
	}

	private static int _runSpecificCommands(String fileName_, Commands commands) {
		// build map from command name to command
		Map nameToCommand = new HashMap();
		Iterator commandIter = commands.getCommandIter();
		while (commandIter.hasNext()) {
			Command curCommand = (Command) commandIter.next();
			if (curCommand.info().name != null) {
				// NOTE: we need to implement a semantic check for duplicate
				// command names
				nameToCommand.put(curCommand.info().name, curCommand);
			}
		}
		// run commands entered at command-line
		Iterator runIter = _commandNames.iterator();
		while (runIter.hasNext()) {
			String curName = (String) runIter.next();
			if (nameToCommand.containsKey(curName)) {
				final int rc = _runCommand(fileName_, (Command) nameToCommand.get(curName));
				if (rc != RC_OK) return rc;
			} else {
				Dbg.warn(curName + " is not the name of a known command.");
			}
		}
		
		return RC_OK;
	}

	private static int _runAllCommands(String fileName_, Commands commands) {
		Iterator commandIter = commands.getCommandIter();
		while (commandIter.hasNext()) {
			Command curCommand = (Command) commandIter.next();
			final int rc = _runCommand(fileName_, curCommand);
			if (rc != RC_OK) return rc;
		}
		return RC_OK;
	}

	/** Run analyzer on the given command, printing results to console. */
	private static int _runCommand(String fileName_, Command command) {
		System.out.println("Analyzing command: " + command);
		AlloyRunner.clearState();

		// how many solutions are we expecting?
		final int numberOfExpectedSolutions;
		final int UNKNOWN_NUMBER_OF_SOLUTIONS_EXPECTED = -1;
		if (command instanceof FindCommand) {
//			final IntNode expects = ((FindCommand)command).getExpects();
//			numberOfExpectedSolutions = !expects.isEmpty() ? expects.getInt() :  UNKNOWN_NUMBER_OF_SOLUTIONS_EXPECTED;
			numberOfExpectedSolutions = command.info().hasExpects() ? command.info().expectsCount() : UNKNOWN_NUMBER_OF_SOLUTIONS_EXPECTED;
		} else {
			numberOfExpectedSolutions =  UNKNOWN_NUMBER_OF_SOLUTIONS_EXPECTED;
		}
        
		boolean foundSolution = false;
		long solutionsOutput = 0; // basically counting the number of iterations
		do {
			final SolutionData solution;
			//final BigInteger solCount = BigInteger.ZERO; // solution counting temporarily disabled

			// step 1.  get the next solution (or the first solution, which is a special case of next)
			if (solutionsOutput == 0) {
				try {
					if (!_countSolutions) {
						final SolutionData solData = AlloyRunner.translateCommand(command);
						if (_astFileName != null) {
							AlloyRunner.writeXML(solData.getFormula(), _astFileName, null); // no node annotator
						}
						solution = AlloyRunner.analyzeCommand(solData, System.currentTimeMillis());

						if (_liftedUnsatCore && solution == null) {
							_printUnsatCore(solData);
						}

					} else {
						//solCount = BigInteger.ZERO;
						solution = null;
						throw new Error("solution counting temporarily disabled");
						// solCount =
						// AlloyRunner.countSolutions(AlloyRunner.translateCommand(command),
						// System.currentTimeMillis(),
						// null /* no list of primary vars */);
					}
				} catch (TranslationException te_) {
					Dbg.fatal("Could not translate: ", te_);
					return RC_TRANSLATION_PROBLEM;
				} catch (alloy.util.EnvFailureException efe) {
					Dbg.fatal("Environment Failure: " + efe);
					return RC_TRANSLATION_PROBLEM;
				}
			} else {
				solution = AlloyRunner.getNextSolution();
			}
			foundSolution = (solution != null);

			// step 2.  process this solution
			if (_countSolutions) {
				throw new Error("solution counting temporarily disabled");
				//System.out.println(solCount + " solutions found");
				//break;
			} else if (solution == null) {
				System.out.println(solutionsOutput == 0 ? "\nNo solution found.\n" : "\nNo more solutions.\n");
				if (numberOfExpectedSolutions > 0) {
					System.out.println("Expected to find at least one solution but didn't.\n");
					return RC_FOUND_SOME_EXPECTED_NONE;
				}
			} else {
				System.out.println("\nSolution #" + (++solutionsOutput) + "\n");
				if (_saveSolutionData) {
					_saveSolution(fileName_, solutionsOutput, solution);
				}

				System.out.println(solution);

				if (numberOfExpectedSolutions == 0) {
					System.out.println("Found a solution but didn't expect one.\n");
					return RC_FOUND_NONE_EXPECTED_SOME;
				}

				// if(_visualize){
				// VizFrame vizFrame = new VizFrame();
				// if (_loadCust) {
				// vizFrame.updateSolution(new File(fileName_).getName(),
				// solution, new File(_custFile));
				// } else {
				// vizFrame.updateSolution(new File(fileName_).getName(),
				// solution);
				// }
				// new Thread(vizFrame).start();
				// }
			}
		} while (foundSolution && (solutionsOutput < _maxSols));
		return RC_OK;
	} // _runCommand()

	private static void _saveSolution(String fileName_, long solutionsOutput, final SolutionData solution) {
		final int dot = fileName_.lastIndexOf(".");
		final int extIndex = dot < 0 ? fileName_.length() : dot;
		try {
			final PrintWriter pw = new PrintWriter(new FileWriter(fileName_.substring(0, extIndex)
					+ Long.toString(solutionsOutput) + ".sol"));
			solution.saveInstance(pw);
			pw.close();
		} catch (IOException ioe) {
			System.out.println("Could not save solution #" + solutionsOutput + "for file" + fileName_ + ioe);
		}
	}

	private static void _printUnsatCore(final SolutionData solData) {
		System.out.println("determining unsat core...");
		final LiftedUnsatCore liftedUnsatCore = AlloyRunner.computeLiftedUnsatCore();
		AlloyRunner.writeXML(solData.getFormula(), "ucore.xml", new alloy.util.Mapper() {
			public Object map(Object obj_) {
				Node n = (Node) obj_;
				return "inCore=" + (liftedUnsatCore.isInCore(n) ? "\"1\"" : "\"0\"");
			}
		});
		System.out.println("Wrote unsat core to ucore.xml");
		// System.out.println("===============begin unsat
		// core===============");
		// ((alloy.ast.FindCommand)command).formula.applyVisitor(new
		// alloy.ast.ASTDepthFirstVisitor() {
		// public void visit(Node node_) {
		// System.out.println((liftedUnsatCore.isInCore(node_) ? "U"
		// : "N") +
		// " " + node_.nodeString());
		// super.visit(node_); // recurse to the children
		// }});
		// System.out.println("================end unsat
		// core===============");
	}

	/**
	 * A message listener that prints error messages in Emacs-style.
	 */
	public static class EmacsMsgListener implements Dbg.DbgMsgListener {

		/** stream to print messages to */
		private java.io.PrintStream _out;

		public EmacsMsgListener(java.io.PrintStream out_) {
			_out = out_;
		}

		/**
		 * Process a debugging message.
		 * 
		 * @param msgType_
		 *            info/warn/error/etc
		 * @param msg_
		 *            error message
		 * @param thrown_
		 *            an exception that was caught -- e.g. an I/O exception was
		 *            caught when trying to open a file, so the exception is
		 *            part of the error message; may be <code>null</code>.
		 */
		public void debugMsg(int msgType_, alloy.util.Msg msg_, Throwable thrown_) {
			StringBuffer msg = new StringBuffer();
			Node node = msg_.node;

			if (node != null && node.getLocation() != Location.UNKNOWN) {
				Location loc = node.getLocation();
				msg.append(loc.getFileName());
				msg.append(":");
				msg.append(loc.getBeginLine());
				msg.append(":");
				msg.append(loc.getBeginColumn() - 1);
				msg.append(":");
				msg.append(loc.getEndLine());
				msg.append(":");
				msg.append(loc.getEndColumn() - 1);
				msg.append(": ");
			}
			msg.append(msg_.message);

			if (node != null && !(node instanceof DummyNode)) {
				msg.append(": ");
				msg.append(node.nodeString());
			}
			_out.println(msg.toString());
		}

		/**
		 * Process a debugging message.
		 * 
		 * @param msgType_
		 *            info/warn/error/etc
		 * @param msg_
		 *            error message
		 * @param thrown_
		 *            an exception that was caught -- e.g. an I/O exception was
		 *            caught when trying to open a file, so the exception is
		 *            part of the error message; may be <code>null</code>.
		 */
		public void debugMsg(int msgType_, String msg_, Throwable thrown_) {
			_out.println(msg_);
		}

	}

} // AlloyCLI

